Skip to content

feat(AlgebraicGeometry/Sites): characterization of sheaves for the P-qc topology#34917

Open
chrisflav wants to merge 7 commits intoleanprover-community:masterfrom
chrisflav:fpqc-topology-1
Open

feat(AlgebraicGeometry/Sites): characterization of sheaves for the P-qc topology#34917
chrisflav wants to merge 7 commits intoleanprover-community:masterfrom
chrisflav:fpqc-topology-1

Conversation

@chrisflav chrisflav added WIP Work in progress t-algebraic-geometry Algebraic geometry labels Feb 6, 2026
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 6, 2026
@github-actions
Copy link

github-actions bot commented Feb 6, 2026

PR summary 8ca4eacd8c

Import changes exceeding 2%

% File
+35.81% Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct 444 603 +159 (+35.81%)
Import changes for all files
Files Import difference
4 files Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Representability
1
Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct 159
Mathlib.AlgebraicGeometry.Sites.Fpqc (new file) 2252

Declarations diff

+ CoproductDisjoint.isPullback_of_isInitial
+ Cover.forgetQc
+ Cover.mem_propqcTopology
+ Cover.ofQuasiCompactCover
+ Cover.qculift
+ Hom.generate_singleton_mem_propqcTopology
+ Hom.singleton_mem_propqcPrecoverage
+ Hom.singleton_mem_qcPrecoverage
+ Presieve.IsSheafFor.of_isSheafFor_pullback
+ Presieve.IsSheafFor.of_isSheafFor_pullback'
+ Presieve.isSheafFor_sigmaDesc_iff
+ Scheme.Cover.Hom.isSheafFor
+ Scheme.Cover.isSheafFor_sigma_iff
+ Scheme.Hom.presieve₀_cover
+ instance : Precoverage.Small.{u} (propqcPrecoverage P)
+ instance {S : Scheme.{u}} (𝒰 : S.AffineCover P) (i : 𝒰.I₀) : IsAffine (𝒰.cover.X i)
+ instance {S : Scheme.{u}} (𝒰 : S.Cover (precoverage P)) [QuasiCompactCover 𝒰.1] :
+ instance {S : Scheme.{u}} [IsAffine S] (𝒰 : S.AffineCover P) [Finite 𝒰.I₀] :
+ isSheaf_propqcTopology_iff
+ mem_propqcPrecoverage_iff_exists_quasiCompactCover
+ ofArrows_ι_mem_zariskiTopology_of_isColimit
+ preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology
+ presieve₀_sigma
+ propqcPrecoverage
+ propqcPrecoverage_le_precoverage
+ propqcTopology
+ zariskiTopology_le_propqcTopology
++ instance {S : Scheme.{u}} (𝒰 : Scheme.Cover (propqcPrecoverage P) S) :

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@chrisflav chrisflav changed the title feat(AlgebraicGeometry/Sites): characterization of sheafs for the P-qc topology feat(AlgebraicGeometry/Sites): characterization of sheaves for the P-qc topology Feb 6, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 6, 2026
@mathlib-merge-conflicts
Copy link

This pull request has conflicts, please merge master and resolve them.

@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 7, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 7, 2026
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 8, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Feb 8, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 9, 2026
@mathlib-merge-conflicts
Copy link

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 13, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 18, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 19, 2026
@mathlib-merge-conflicts
Copy link

This pull request has conflicts, please merge master and resolve them.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebraic-geometry Algebraic geometry WIP Work in progress

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

Comments